On inductive types in homotopy type theory via homotopy-initial algebras over an endofunctor:
Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICS’12: (2012) 95–104 [arXiv:1201.3898, doi:10.1109/LICS.2012.21, Coq code]
Exposition:
Steve Awodey, Inductive types in HoTT (Jan 2012) [blog post]
and analogously on higher inductive types:
Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31–42 [arXiv:1402.0761, doi:10.1145/2775051.2676983]
Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1–45 [arXiv:1504.05531, doi:10.1145/3006383]
On the Eckmann-Hilton argument in homotopy type theory:
Last revised on December 26, 2022 at 22:26:59. See the history of this page for a list of all contributions to it.